package edu.uic.cs.cs582.process.impl;

import java.util.ArrayList;
import java.util.Arrays;
import java.util.Collection;
import java.util.Collections;
import java.util.Comparator;
import java.util.LinkedList;
import java.util.List;
import java.util.Map.Entry;
import java.util.Set;
import java.util.TreeSet;

import org.apache.commons.collections.primitives.ArrayIntList;
import org.apache.commons.collections.primitives.IntList;
import org.apache.commons.lang.StringUtils;

import edu.mit.jwi.item.POS;
import edu.uic.cs.cs582.data.Component;
import edu.uic.cs.cs582.data.Polarity;
import edu.uic.cs.cs582.data.Synset;
import edu.uic.cs.cs582.data.Word;
import edu.uic.cs.cs582.misc.Assert;
import edu.uic.cs.cs582.process.CnfGenerator;

public class AddingFrequencyCnfGeneratorImpl extends
		AbstractBasicVariablesGeneratorImpl implements CnfGenerator
{

	AddingFrequencyCnfGeneratorImpl(Component component)
	{
		super(component);
	}

	@Override
	public Set<int[]> generateCnfs(POS pos, Word word, Polarity polarity)
	{
		Set<int[]> result = new TreeSet<int[]>(new IntArrayComparator());
		int halfFrequencySum = word.getFrequencySum() / 2;

		if (polarity != Polarity.NEUTRAL)
		{
			// Step 2 and 3
			LinkedList<IntList> frequencyDigitsQueue = generateAndStoreFrequencyBitCnfsForNonNeutralWord(
					word, polarity, result);

			// step 4
			IntList finalFrequencySummationDigits = generateAndStoreAdditionExpression(
					word, frequencyDigitsQueue, result);

			// step 5
			Collection<int[]> greaterThanHalfExpression = generateCnfForSummationGreaterThanValue(
					finalFrequencySummationDigits, halfFrequencySum);
			result.addAll(greaterThanHalfExpression);
		}
		else
		{
			// Step 2 and 3
			LinkedList<IntList> frequencyDigitsQueue = generateAndStoreFrequencyBitCnfsForNeutralWord(
					word, result);

			// step 4
			IntList finalFrequencySummationDigits = generateAndStoreAdditionExpression(
					word, frequencyDigitsQueue, result);

			// step 5
			Collection<int[]> lessThanOrEqualsToHalfExpression = /*generateCnfForSummationLessThanOrEqualsToValue*/generateCnfForSummationGreaterThanValue(
					finalFrequencySummationDigits, halfFrequencySum);

			result.addAll(lessThanOrEqualsToHalfExpression);
		}

		return result;
	}

	/**
	 *  -------------------------
	 * |Step 4 in my report|
	 *  -------------------------
	 *  
	 */
	private IntList generateAndStoreAdditionExpression(Word word,
			LinkedList<IntList> frequencyDigitsQueue, Set<int[]> result)
	{
		// step 4
		Collection<int[]> additionExpression = generateCnfForFrequencyAddition(
				frequencyDigitsQueue, word);
		result.addAll(additionExpression);

		Assert.isTrue(frequencyDigitsQueue.size() == 1);
		IntList finalFrequencySummationDigits = frequencyDigitsQueue.poll();
		Assert.isTrue(finalFrequencySummationDigits.size() >= Integer
				.toBinaryString(word.getFrequencySum()).length());

		return finalFrequencySummationDigits;
	}

	private LinkedList<IntList> generateAndStoreFrequencyBitCnfsForNeutralWord(
			Word word, Set<int[]> result)
	{
		// stores all the frequency-digit variables for each synset of current word
		LinkedList<IntList> frequencyDigits = new LinkedList<IntList>();

		int wordIndexInComponent = component.getIndexOfWord(word);
		int variableIndexBase = 0;
		for (Entry<Synset, Integer> frequencyBySynset : word
				.getFrequenciesBySynsetRelateTo().entrySet())
		{
			Synset synset = frequencyBySynset.getKey();
			int frequency = frequencyBySynset.getValue();
			// NOTICE! reverse order!
			String frequencyBinaryString = StringUtils.reverse(Integer
					.toBinaryString(frequency));

			Collection<int[]> cnfForOneFrequency = generateCnfForOneNeutralFrequency(
					synset, frequencyBinaryString, variableIndexBase,
					wordIndexInComponent, frequencyDigits);
			result.addAll(cnfForOneFrequency);

			variableIndexBase += frequencyBinaryString.length();
		}

		Assert.isTrue(word.getTotalFrequencyDigitNumber() == variableIndexBase);

		return frequencyDigits;
	}

	/**
	 * If s is NEUTRAL
	 * 
	 * suppose x = (110) in binary form
	 * 
	 * 	   ((¬s+ AND ¬s-) -> (x12=1) AND (x11=1) AND (x10=0))
	 * AND ((s+ OR s-) -> (x12=0) AND (x11=0) AND (x10=0))
	 * 	
	 * ⇔      ((s+ OR s-) OR (x12 AND x11 AND ¬x10))
	 * AND ((¬s+ AND ¬s-) OR (¬x12 AND ¬x11 AND ¬x10))
	 * 
	 * ⇔      (s+ OR s- OR x12)
	 * AND (s+ OR s- OR x11)
	 * AND (s+ OR s- OR ¬x10)
	 * 
	 * AND [DNF]((¬s+ AND ¬s-) OR (¬x12 AND ¬x11 AND ¬x10))
	 * 
	 */
	private Collection<int[]> generateCnfForOneNeutralFrequency(Synset synset,
			String frequencyBinaryString, int variableIndexBase,
			int wordIndexInComponent, LinkedList<IntList> frequencyDigits)
	{
		List<int[]> result = new ArrayList<int[]>(
				frequencyBinaryString.length());
		////////////////////////////////////////////////////////////////////////

		// store all the indices for each digit of a frequency for current word 
		IntList frequencyDigitIndices = new ArrayIntList(
				frequencyBinaryString.length());
		// put the frequency digits for one synset of a current word
		frequencyDigits.add(frequencyDigitIndices);
		////////////////////////////////////////////////////////////////////////

		int indexOfSynsetInTheComponent = component.getIndexOfSynset(synset);
		// s+
		int positiveSynsetIndexSymbol = polarSymbol(Polarity.POSITIVE,
				indexOfSynsetInTheComponent);
		// ¬s+
		int notPositiveSynsetIndexSymbol = not(positiveSynsetIndexSymbol);
		// s-
		int negativeSynsetIndexSymbol = polarSymbol(Polarity.NEGATIVE,
				indexOfSynsetInTheComponent);
		// ¬s-
		int notNegativeSynsetIndexSymbol = not(negativeSynsetIndexSymbol);
		////////////////////////////////////////////////////////////////////////

		int[] clause = null;
		int length = frequencyBinaryString.length() + variableIndexBase;
		for (int variableIndex = variableIndexBase; variableIndex < length; variableIndex++)
		{
			// x1
			int frequencyDigitVariableSymbol = frequencyDigitSymbol(
					variableIndex, wordIndexInComponent);
			// store this digit ////////////////////////////////////////////////
			frequencyDigitIndices.add(frequencyDigitVariableSymbol);
			////////////////////////////////////////////////////////////////////

			/**
			 *  ⇔   (s+ OR s- OR x12)
			 * AND (s+ OR s- OR x11)
			 * AND (s+ OR s- OR ¬x10)
			 */
			// (s+ OR s- OR ¬x10)
			if (frequencyBinaryString.charAt(variableIndex - variableIndexBase) == '0')
			{
				clause = new int[] {
						positiveSynsetIndexSymbol,
						negativeSynsetIndexSymbol,
						not(frequencyDigitVariableSymbol) };
				result.add(clause);
			}
			// (s+ OR s- OR x12)
			else
			{
				clause = new int[] {
						positiveSynsetIndexSymbol,
						negativeSynsetIndexSymbol,
						frequencyDigitVariableSymbol };
				result.add(clause);
			}
		}

		/**
		 * [DNF]((¬s+ AND ¬s-) OR (¬x12 AND ¬x11 AND ¬x10))
		 */
		List<int[]> secondHalfExpressionInDnf = new ArrayList<int[]>(2);
		// (¬s+ AND ¬s-)
		secondHalfExpressionInDnf.add(new int[] {
				notPositiveSynsetIndexSymbol,
				notNegativeSynsetIndexSymbol });
		// (¬x12 AND ¬x11 AND ¬x10)
		int[] notAndClause = new int[frequencyDigitIndices.size()];
		for (int index = 0; index < frequencyDigitIndices.size(); index++)
		{
			notAndClause[index] = not(frequencyDigitIndices.get(index));
		}
		secondHalfExpressionInDnf.add(notAndClause);

		Set<int[]> secondHalfExpressionInCnf = convertDnfToCnf(secondHalfExpressionInDnf);
		result.addAll(secondHalfExpressionInCnf);

		return result;
	}

	/**
	 *  -------------------------
	 * |Step 2 and 3 in my report|
	 *  -------------------------
	 *  
	 */
	private LinkedList<IntList> generateAndStoreFrequencyBitCnfsForNonNeutralWord(
			Word word, Polarity polarity, Set<int[]> result)
	{
		// stores all the frequency-digit variables for each synset of current word
		LinkedList<IntList> frequencyDigits = new LinkedList<IntList>();

		int wordIndexInComponent = component.getIndexOfWord(word);
		int variableIndexBase = 0;
		for (Entry<Synset, Integer> frequencyBySynset : word
				.getFrequenciesBySynsetRelateTo().entrySet())
		{
			Synset synset = frequencyBySynset.getKey();
			int frequency = frequencyBySynset.getValue();
			// NOTICE! reverse order!
			String frequencyBinaryString = StringUtils.reverse(Integer
					.toBinaryString(frequency));

			Collection<int[]> cnfForOneFrequency = generateCnfForOneNonNeutralFrequency(
					polarity, synset, frequencyBinaryString, variableIndexBase,
					wordIndexInComponent, frequencyDigits);
			result.addAll(cnfForOneFrequency);

			variableIndexBase += frequencyBinaryString.length();
		}

		Assert.isTrue(word.getTotalFrequencyDigitNumber() == variableIndexBase);

		return frequencyDigits;
	}

	/**
	 * 
	 *  -------------------------
	 * |Step 2 and 3 in my report|
	 *  -------------------------
	 *  
	 *
	 * Suppose w1 is POSITIVE 
	 * and one synset s1’s frequency is 6 = (110)_bin.
	 *
	 *	   (s1+ -> (x12=1) AND (x11=1) AND (x10=0))
	 * AND (¬s1+ -> (x12=0) AND (x11=0) AND (x10=0)
	 * 	
	 * ⇔      (¬s1+ OR (x12 AND x11 AND ¬x10))
	 * AND (s1+ OR (¬x12 AND ¬x11 AND ¬x10))
	 * 
	 * ⇔      (¬s1+ OR ¬x10)
	 * AND (¬s1+ OR x11)
	 * AND (¬s1+ OR x12)
	 * 
	 * AND (s1+ OR ¬x10)
	 * AND (s1+ OR ¬x11) 
	 * AND (s1+ OR ¬x12)
	 * 
	 * ⇔      (¬s1+ OR ¬x10)
	 * AND (s1+ OR ¬x10)
	 * 
	 * AND (¬s1+ OR x11)
	 * AND (s1+ OR ¬x11) 
	 * 
	 * AND (¬s1+ OR x12)
	 * AND (s1+ OR ¬x12)
	 * 
	 */
	private List<int[]> generateCnfForOneNonNeutralFrequency(
			Polarity wordPolarity, Synset synset, String frequencyBinaryString,
			int variableIndexBase, int wordIndexInComponent,
			List<IntList> frequencyDigits)
	{
		int indexOfSynsetInTheComponent = component.getIndexOfSynset(synset);

		List<int[]> result = new ArrayList<int[]>(
				frequencyBinaryString.length());

		////////////////////////////////////////////////////////////////////////
		// store all the indices for each digit of a frequency for current word 
		IntList frequencyDigitIndices = new ArrayIntList(
				frequencyBinaryString.length());
		// put the frequency digits for one synset of a current word
		frequencyDigits.add(frequencyDigitIndices);
		////////////////////////////////////////////////////////////////////////

		int length = frequencyBinaryString.length() + variableIndexBase;
		// s1+
		int synsetIndexSymbol = polarSymbol(wordPolarity,
				indexOfSynsetInTheComponent);
		// ¬s1+
		int synsetNotIndexSymbol = not(synsetIndexSymbol);
		int[] clause = null;
		for (int variableIndex = variableIndexBase; variableIndex < length; variableIndex++)
		{
			// x11
			int frequencyDigitVariableSymbol = frequencyDigitSymbol(
					variableIndex, wordIndexInComponent);
			// store this digit ////////////////////////////////////////////////
			frequencyDigitIndices.add(frequencyDigitVariableSymbol);
			////////////////////////////////////////////////////////////////////

			// ¬x11
			int frequencyDigitVariableSymbolNotSymbol = not(frequencyDigitVariableSymbol);

			//  (¬s1+ OR ¬x10)
			if (frequencyBinaryString.charAt(variableIndex - variableIndexBase) == '0')
			{
				clause = generateSynsetORVariableClause(synsetNotIndexSymbol,
						frequencyDigitVariableSymbolNotSymbol);
				result.add(clause);
			}
			// (¬s1+ OR x11)
			else
			{
				clause = generateSynsetORVariableClause(synsetNotIndexSymbol,
						frequencyDigitVariableSymbol);
				result.add(clause);
			}

			// (s1+ OR ¬x10) || (s1+ OR ¬x11) 
			clause = generateSynsetORVariableClause(synsetIndexSymbol,
					frequencyDigitVariableSymbolNotSymbol);
			result.add(clause);

		}

		return result;
	}

	private int[] generateSynsetORVariableClause(int synsetIndexSymbol,
			int variableSymbol)
	{
		int[] clause = new int[2];

		// Remember in sorted order
		if (variableSymbol > synsetIndexSymbol)
		{
			clause[0] = synsetIndexSymbol;
			clause[1] = variableSymbol;
		}
		else
		{
			clause[0] = variableSymbol;
			clause[1] = synsetIndexSymbol;
		}

		return clause;
	}

	////////////////////////////////////////////////////////////////////////////

	/**
	 *  -------------------
	 * |Step 4 in my report|
	 *  -------------------
	 *  
	 * @param frequencyDigitsQueue initially it stores digit variables for each frequency
	 * @param nextDigitIndex index for the next generating variable,
	 *  which may be carrier or summation digit
	 * @return
	 */
	private Collection<int[]> generateCnfForFrequencyAddition(
			LinkedList<IntList> frequencyDigitsQueue, Word word)
	{
		// ordered by size in order to let those two with same size process first, 
		// and hence reduce the number of variables. e.g.,
		//     abc : def = 3; hijk : lmno = 4; 3 : 4 = 4 ; total = 3+4+4 = 11
		// BUT, abc : hijk = 4;  def: lmno = 4; 4 : 4 = 4; total = 4+4+4 = 12
		Comparator<IntList> queueSizeSorter = new Comparator<IntList>()
		{
			@Override
			public int compare(IntList o1, IntList o2)
			{
				// order by size
				return o1.size() - o2.size();
			}
		};
		Collections.sort(frequencyDigitsQueue, queueSizeSorter);
		////////////////////////////////////////////////////////////////////////

		int nextDigitIndex = word.getTotalFrequencyDigitNumber();
		int wordIndex = component.getIndexOfWord(word);

		/**
		 * 					x_i+1	x_i	...	x_1	x_0
		 * 			y_i+2	y_i+1	y_i	...	y_1	y_0
		 * ----------------------------------------
		 * c_i+3	c_i+2	c_i+1	c_i	...	c_1	 /
		 * s_i+3	s_i+2	s_i+1	s_i	...	s_1	s_0
		 */
		TreeSet<int[]> result = new TreeSet<int[]>(new IntArrayComparator());

		IntList first = null;
		IntList second = null;
		while ((first = frequencyDigitsQueue.poll()) != null)
		{
			if ((second = frequencyDigitsQueue.poll()) != null)
			{
				Assert.isTrue(!first.isEmpty());
				Assert.isTrue(!second.isEmpty());

				IntList frequencySummationDigits = new ArrayIntList(
						second.size() + 1);

				// second's size always >= first since they have been sorted
				// For carries: 	  1, 2, 3, ..., sizeOfFirst ~ total sizeOfFirst
				// For summations: 0, 1, 2, 3, ..., ..., ..., sizeOfSecond ~ total (sizeOfSecond+1)
				int c_previous = 0;
				int c_current = 0;
				for (int index = 0; index < (second.size() + 1); index++)
				{
					if (index != 0)
					{
						// c_i
						c_current = frequencyDigitSymbol(nextDigitIndex++,
								wordIndex);
						generateAndStoreCarries(index, first, second,
								c_previous, c_current, result);
						c_previous = c_current;
					}

					//s_i
					int s_current = frequencyDigitSymbol(nextDigitIndex++,
							wordIndex);
					generateAndStoreSummations(index, first, second, c_current,
							s_current, result);

					frequencySummationDigits.add(s_current);
				}

				// queue the new frequency summation digits for one synset of a current word
				frequencyDigitsQueue.offer(frequencySummationDigits);
				// then resort it by size
				Collections.sort(frequencyDigitsQueue, queueSizeSorter);
			}
			else
			{
				// first is the last final one in the queue
				// put it back into the queue for step 5's usage
				frequencyDigitsQueue.offer(first);
				break;
			}
		}

		return result;
	}

	private void generateAndStoreSummations(int index, IntList first,
			IntList second, int c_current, int s_current, Set<int[]> result)
	{
		if (index == 0)
		{
			// DO NOT use c_current since c_0 = '0'
			int x_0 = first.get(0);
			int y_0 = second.get(0);
			generateAndStoreFirstSummation(x_0, y_0, s_current, result);
		}
		else if (index < first.size())
		{
			Assert.isTrue(c_current != 0);
			int x_current = first.get(index);
			int y_current = second.get(index);
			generateAndStoreTwoAddendsSummation(x_current, y_current,
					c_current, s_current, result);
		}
		else if (index < second.size())
		{
			Assert.isTrue(c_current != 0);
			int y_current = second.get(index);
			generateAndStoreOneAddendSummation(y_current, c_current, s_current,
					result);
		}
		else
		{
			Assert.isTrue(c_current != 0);
			generateAndStoreLastSummation(c_current, s_current, result);

		}

	}

	/**
	 * s_0
	 */
	private void generateAndStoreFirstSummation(int x_0, int y_0, int s_0,
			Set<int[]> result)
	{
		// 1st half expression
		ArrayList<int[]> firstHalfExpressionInDnf = new ArrayList<int[]>();
		firstHalfExpressionInDnf.add(new int[] { not(s_0) });
		firstHalfExpressionInDnf.add(new int[] { not(x_0), y_0 });
		firstHalfExpressionInDnf.add(new int[] { x_0, not(y_0) });
		Set<int[]> firstHalfExpressionInCnf = convertDnfToCnf(firstHalfExpressionInDnf);
		result.addAll(firstHalfExpressionInCnf);

		// 2nd half expression
		int[] cnfClause = null;

		cnfClause = new int[] { s_0, x_0, not(y_0) };
		Arrays.sort(cnfClause);
		result.add(cnfClause);

		cnfClause = new int[] { s_0, not(x_0), y_0 };
		Arrays.sort(cnfClause);
		result.add(cnfClause);
	}

	private void generateAndStoreTwoAddendsSummation(int x_current,
			int y_current, int c_current, int s_current, Set<int[]> result)
	{
		// 1st half expression
		ArrayList<int[]> firstHalfExpressionInDnf = new ArrayList<int[]>();
		firstHalfExpressionInDnf.add(new int[] { not(s_current) });
		firstHalfExpressionInDnf.add(new int[] {
				not(x_current),
				not(y_current),
				c_current });
		firstHalfExpressionInDnf.add(new int[] {
				not(x_current),
				y_current,
				not(c_current) });
		firstHalfExpressionInDnf.add(new int[] {
				x_current,
				not(y_current),
				not(c_current) });
		firstHalfExpressionInDnf.add(new int[] {
				x_current,
				y_current,
				c_current });
		Set<int[]> firstHalfExpressionInCnf = convertDnfToCnf(firstHalfExpressionInDnf);
		result.addAll(firstHalfExpressionInCnf);

		// 2nd half expression
		int[] cnfClause = null;

		cnfClause = new int[] { s_current, not(x_current), y_current, c_current };
		Arrays.sort(cnfClause);
		result.add(cnfClause);

		cnfClause = new int[] { s_current, x_current, not(y_current), c_current };
		Arrays.sort(cnfClause);
		result.add(cnfClause);

		cnfClause = new int[] { s_current, x_current, y_current, not(c_current) };
		Arrays.sort(cnfClause);
		result.add(cnfClause);

		cnfClause = new int[] {
				s_current,
				not(x_current),
				not(y_current),
				not(c_current) };
		Arrays.sort(cnfClause);
		result.add(cnfClause);
	}

	private void generateAndStoreOneAddendSummation(int y_current,
			int c_current, int s_current, Set<int[]> result)
	{
		// 1st half expression
		ArrayList<int[]> firstHalfExpressionInDnf = new ArrayList<int[]>();
		firstHalfExpressionInDnf.add(new int[] { not(s_current) });
		firstHalfExpressionInDnf.add(new int[] { not(y_current), c_current });
		firstHalfExpressionInDnf.add(new int[] { y_current, not(c_current) });
		Set<int[]> firstHalfExpressionInCnf = convertDnfToCnf(firstHalfExpressionInDnf);
		result.addAll(firstHalfExpressionInCnf);

		// 2nd half expression
		int[] cnfClause = null;

		cnfClause = new int[] { s_current, not(y_current), c_current };
		Arrays.sort(cnfClause);
		result.add(cnfClause);

		cnfClause = new int[] { s_current, y_current, not(c_current) };
		Arrays.sort(cnfClause);
		result.add(cnfClause);

	}

	private void generateAndStoreLastSummation(int c_current, int s_current,
			Set<int[]> result)
	{
		int[] cnfClause = null;

		cnfClause = new int[] { s_current, not(c_current) };
		Arrays.sort(cnfClause);
		result.add(cnfClause);

		cnfClause = new int[] { not(s_current), c_current };
		Arrays.sort(cnfClause);
		result.add(cnfClause);
	}

	//////////////////////////////////

	// For carries: 	  1, 2, 3, ..., sizeOfFirst ~ total sizeOfFirst
	// addendIndex:    0, 1, 2, 3, ..., ..., ..., sizeOfSecond
	private void generateAndStoreCarries(int index, IntList first,
			IntList second, int c_previous, int c_current, Set<int[]> result)
	{
		if (index == 1)
		{
			int x_0 = first.get(0);
			int y_0 = second.get(0);
			// DO NOT use c_previous here since c_0 = '0'!
			generateAndStoreFirstCarry(x_0, y_0, c_current, result);
		}
		else if (index <= first.size())
		{
			Assert.isTrue(c_previous != 0);
			int x_previous = first.get(index - 1);
			int y_previous = second.get(index - 1);

			generateAndStoreMiddleCarries(x_previous, y_previous, c_previous,
					c_current, result);
		}
		else
		{
			Assert.isTrue(c_previous != 0);
			int y_previous = second.get(index - 1);
			generateAndStoreLastCarry(y_previous, c_previous, c_current, result);
		}
	}

	private void generateAndStoreFirstCarry(int x_0, int y_0, int c_1,
			Set<int[]> result)
	{
		// c_previous/c_0 equals to '0', so there's no c_0 variable
		int[] cnfClause = new int[] { not(c_1), x_0 };
		Arrays.sort(cnfClause);
		result.add(cnfClause);

		cnfClause = new int[] { not(c_1), y_0 };
		Arrays.sort(cnfClause);
		result.add(cnfClause);

		cnfClause = new int[] { c_1, not(x_0), not(y_0) };
		Arrays.sort(cnfClause);
		result.add(cnfClause);
	}

	private void generateAndStoreMiddleCarries(int x_previous, int y_previous,
			int c_previous, int c_current, Set<int[]> result)
	{
		// 1st half expression
		ArrayList<int[]> firstHalfExpressionInDnf = new ArrayList<int[]>();
		firstHalfExpressionInDnf.add(new int[] { not(c_current) });
		firstHalfExpressionInDnf.add(new int[] { x_previous, y_previous });
		firstHalfExpressionInDnf.add(new int[] { x_previous, c_previous });
		firstHalfExpressionInDnf.add(new int[] { y_previous, c_previous });
		Set<int[]> firstHalfExpressionInCnf = convertDnfToCnf(firstHalfExpressionInDnf);
		result.addAll(firstHalfExpressionInCnf);

		// 2nd half expression
		int[] cnfClause = null;

		cnfClause = new int[] { not(x_previous), not(y_previous), c_current };
		Arrays.sort(cnfClause);
		result.add(cnfClause);

		cnfClause = new int[] { not(x_previous), not(c_previous), c_current };
		Arrays.sort(cnfClause);
		result.add(cnfClause);

		cnfClause = new int[] { not(y_previous), not(c_previous), c_current };
		Arrays.sort(cnfClause);
		result.add(cnfClause);

	}

	private void generateAndStoreLastCarry(int y_previous, int c_previous,
			int c_current, Set<int[]> result)
	{
		int[] cnfClause = null;

		// 1st half expression
		cnfClause = new int[] { not(c_current), y_previous };
		Arrays.sort(cnfClause);
		result.add(cnfClause);

		cnfClause = new int[] { not(c_current), c_previous };
		Arrays.sort(cnfClause);
		result.add(cnfClause);

		// 2nd half expression
		cnfClause = new int[] { not(y_previous), not(c_previous), c_current };
		Arrays.sort(cnfClause);
		result.add(cnfClause);

	}

	////////////////////////////////////////////////////////////////////////////

	private Collection<int[]> generateCnfForSummationLessThanOrEqualsToValue(
			IntList finalFrequencySummationDigits, int value)
	{
		int totalSummationDigitsNumber = finalFrequencySummationDigits.size();
		// NOTICE! reverse order!
		String valueBinaryString = StringUtils.reverse(Integer
				.toBinaryString(value));
		int valueBinaryStringLength = valueBinaryString.length();
		Assert.isTrue(
				totalSummationDigitsNumber >= valueBinaryStringLength,
				"The number of total ["
						+ totalSummationDigitsNumber
						+ "] bits for summation must greater than or equals to the number of bits for value["
						+ value + "(" + Integer.toBinaryString(value) + ")]. ");

		Collection<int[]> greaterThanInCnf = generateCnfForSummationGreaterThanValue(
				finalFrequencySummationDigits, value);
		for (int[] eachClause : greaterThanInCnf)
		{
			for (int index = 0; index < eachClause.length; index++)
			{
				eachClause[index] = not(eachClause[index]);
			}
		}
		List<int[]> notGreaterThanInDnf = new ArrayList<int[]>(greaterThanInCnf);

		return convertDnfToCnf(notGreaterThanInDnf);

	}

	/**
	 *  -------------------
	 * |Step 5 in my report|
	 *  -------------------
	 *  
	 * @param finalFrequencySummationDigits
	 * @param value
	 * @return
	 */
	private Collection<int[]> generateCnfForSummationGreaterThanValue(
			IntList finalFrequencySummationDigits, int value)
	{
		int totalSummationDigitsNumber = finalFrequencySummationDigits.size();
		// NOTICE! reverse order!
		String valueBinaryString = StringUtils.reverse(Integer
				.toBinaryString(value));
		int valueBinaryStringLength = valueBinaryString.length();
		Assert.isTrue(
				totalSummationDigitsNumber >= valueBinaryStringLength,
				"The number of bits for summation["
						+ totalSummationDigitsNumber
						+ "]bits must greater than or equals to the number of bits for value["
						+ value + "]. ");

		ArrayList<IntList> allCnfClauses = new ArrayList<IntList>();

		// drop first '1's
		int index = 0;
		while (index < valueBinaryStringLength
				&& valueBinaryString.charAt(index) == '1')
		{
			index++;
		}
		ArrayIntList intList = new ArrayIntList();
		allCnfClauses.add(intList);
		////////////////////////////////////////////////////////////////////////

		for (; index < totalSummationDigitsNumber; index++)
		{
			if (index < valueBinaryStringLength
					&& valueBinaryString.charAt(index) == '1')
			{
				intList = new ArrayIntList();
				intList.add(finalFrequencySummationDigits.get(index));
				allCnfClauses.add(intList);
			}
			else
			{
				for (IntList eachClause : allCnfClauses)
				{
					eachClause.add(finalFrequencySummationDigits.get(index));
				}
			}
		}

		Set<int[]> result = new TreeSet<int[]>(new IntArrayComparator());
		int[] clauseArray = null;
		for (IntList clause : allCnfClauses)
		{
			clauseArray = clause.toArray();
			Arrays.sort(clauseArray);
			result.add(clauseArray);
		}

		return result;
	}

	public static void main(String[] args)
	{
		AddingFrequencyCnfGeneratorImpl impl = new AddingFrequencyCnfGeneratorImpl(
				null);
		IntList finalFrequencySummationDigits = new ArrayIntList();
		finalFrequencySummationDigits.add(0);
		finalFrequencySummationDigits.add(1);
		finalFrequencySummationDigits.add(2);
		finalFrequencySummationDigits.add(3);

		for (int index = 0; index < 16; index++)
		{
			Collection<int[]> result = impl
					.generateCnfForSummationGreaterThanValue(
							finalFrequencySummationDigits, index);
			System.out.print(index + ": ");
			for (int[] each : result)
			{
				System.out.print(Arrays.toString(each) + " /\\ ");
			}

			result = impl.generateCnfForSummationLessThanOrEqualsToValue(
					finalFrequencySummationDigits, index);
			System.out.print("		");
			for (int[] each : result)
			{
				System.out.print(Arrays.toString(each) + " \\/ ");
			}

			System.out.println();
		}

		System.out.println("==============================================");
		ArrayList<int[]> dnfs = new ArrayList<int[]>();
		dnfs.add(new int[] { 0 });
		dnfs.add(new int[] { 1 });
		dnfs.add(new int[] { 2 });
		dnfs.add(new int[] { 3 });
		Set<int[]> result = impl.convertDnfToCnf(dnfs);
		for (int[] each : result)
		{
			System.out.println(Arrays.toString(each));
		}

		System.out.println("==============================================");
		IntList first = new ArrayIntList();
		first.add(1);
		IntList second = new ArrayIntList();
		second.add(2);
		result = new TreeSet<int[]>(new IntArrayComparator());
		impl.generateAndStoreSummations(0, first, second, 0, 3, result);

		for (int[] each : result)
		{
			System.out.println(Arrays.toString(each));
		}
	}
}
